00050	(SETQ NEGSGN @¬)
00100	
00150	
00200	
00250	(DEFPROP THSET
00300	   (LAMBDA(A B)
00350		(EVAL(LIST @THSETQ A(LIST @QUOTE B)T T)))
00400	EXPR)
00450	
00500	(DEFPROP THVSET
00550	   (LAMBDA(A B)
00600		(EVAL(LIST @THVSETQ A(LIST @QUOTE B))))
00650	EXPR)
00670	
00672	
00674	(DEFPROP GETNUMARG
00676	   (LAMBDA(X)
00678		(COND((EQ(CAR X)@#)(CAADDR X))
00680		     (T(CAR X)))  )
00682	EXPR)
00684	
00686	
00700	
00702	
00704	(DEFPROP NEWVAR
00708	   (LAMBDA(X)
00712	      (PROG (XT)
00713		(SETQ XT X)
00714	NE1	(THSET (CAR XT)(READLIST(APPEND(LIST @X)(EXPLODE(THSETQ(THV XN)(ADD1(THV XN)))))))
00717		(THVAL(LIST @THASSERT(LIST @ISVAR (CAR XT)))THALIST)
00719		(SETQ XT(CDR XT))
00721		(COND(XT(GO NE1))) 
00722		(RETURN T)   ))
00724	FEXPR)
00728	
00732	
00734	(DEFPROP GZ
00736	   (LAMBDA(X)
00738		(AND(NOT(MINUSP (CAR X)))(NOT(ZEROP (CAR X)))) )
00740	EXPR)
00742	
00744	(DEFPROP GT
00746	   (LAMBDA(X Y)
00748		(*GREAT (CAR X)(CAR Y)) )
00750	EXPR)
00752	
00754	
00756	(DEFPROP SUB2
00758	   (LAMBDA(X)
00760		(SUB1(SUB1 X))  )
00762	EXPR)
00764	
00766	
00800	
00850	(SETQ ADVBRL @((FOR . AD1)(DELETE . AD2)(ADD . AD3)(ALTER . AD4)(ASSUME . AD5)
00900		       (RESTRICT . AD6)(ADVICE . AD7)(STATUS . AD8)))
00950	
01000	
01050	(DEFPROP ADVICESYS
01100	   (LAMBDA NIL
01150	      (PROG(ADV ALR NA OPT LL VN)
01200		(TERPRI)(PRINT @*********___ENTERING__ADVICE__SYSTEM___*********)(TERPRI)
01250		(SETQ SSW T)
01300	AD01	(SETQ OPT NIL)
01350		(PRINT(READLIST(APPEND @(#)(EXPLODE(ADD1 AN)))))
01400		(SETQ ADV(READ))
01450		(COND((NULL ADV) (SETQ SSW NIL) (RETURN NIL)))
01500		(COND((EQ ADV T)(SETQ SSW NIL) (RETURN T)))
01550		(SETQ AN(ADD1 AN))
01600		(SETQ ADV(LIST ADV AN))
01650		(SETQ NA(ASSOC(CAR ADV)ADVBRL))
01700		(COND(NA(GO(CDR NA)))
01750		     (T(SETQ AN(SUB1 AN))(PRINT @NONESENSE!!)(GO AD01)))
01800	AD1	(SETQ ADV(CONS(READ)ADV))
01850		(SETQ NA(CAR ADV))
01900		(SETQ ADV(CONS(READ)ADV))
01950		(COND((EQ @FIRST(CAR ADV))(SETQ OPT T)
02000		      (SETQ ADV(CONS(READ)ADV)) ))
02050		(SETQ ADV(CONS(CONS(READ)(READ))ADV))
02100		(SETQ AL(CONS(REVERSE ADV)AL))
02150		(COND((NULL OPT)(RPLACD(FBODY(GET NA @THEOREM))
02200				(LIST(LIST @THOR(CONS @THAND(CDR(FBODY(GET NA @THEOREM))))
02250						(LIST @THGOAL(APPEND(CAR ADV)@(R))@(THTBF FILTEROP))))))
02300	
02350		     (T(RPLACD(FBODY(GET NA @THEOREM))
02400			      (CONS(LIST @THGOAL(APPEND(CAR ADV)@(R))@(THTBF FILTEROP))
02450				   (CDR(FBODY(GET NA @THEOREM)))))))
02500		(PRINT @IS_RULE_DEFINED_FOR_GIVEN_ADVICE?*)
02550		(COND((READ)(GO AD01)))
02600	AD02	(PRINT @DEFINITION_FILENAME_)(PRINC @(ENCLOSE IN PARENS PLEASE))(PRINC @*)
02650		(SETQ LL(READ))
02660		(COND((AND(NOT(NULL LL))(NOT(EQ @DSK:(CAR LL))))(SETQ FILENAME(CAR LL))(GO AD002)))
02700		(COND((NULL COMPI)(DSKIN COMPR)(ED T)(SETQ COMPI T)))
02750		(COMP LL)
02755	AD002	(SETQ VN(THV ZN))
02760		(EVAL(LIST @DSKIN FILENAME))
02770		(COND((AND(NOT(NULL LL))(NOT(EQ @DSK:(CAR LL))))(RESTOREPROP)(REMPROP @RESTOREPROP @EXPR)))
02773		(THSETQ(THV ZN)(PLUS VN 10))
02776		(THSETQ(THV YN)(PLUS VN 10))
02779		(THSETQ(THV XN)(PLUS VN 10))
02800		(GO AD01)
02850	AD2	(SETQ NA(READ))
02900		(COND((GET NA @THEOREM)(THVAL(LIST @THERASE NA)THALIST))
02950		     ((EQ @#(CAR(EXPLODE NA)))(DELAD NA)(GO AD01))
03000		     ((EQ NEGSGN(CAR(EXPLODE NA)))
03050		      (COND((GET(READLIST(CDR(EXPLODE NA)))@PARTIAL)(SETQ NA(READLIST(APPEND @(N)(CDR(EXPLODE NA)))))
03100			    (COND((GET(READLIST(CDR(EXPLODE NA)))@FLUENT)
03150				  (SETQ NA(CONS NA(APPEND(READ)@(R)))))
03200				 (T(SETQ NA(CONS NA(READ)))))
03250			    (COND((THVAL @(THGOAL(THEV NA))THALIST)(THVAL @(THERASE(THEV NA))THALIST))))
03300			   (T(SETQ NA(READLIST(CDR(EXPLODE NA))))
03350			     (COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
03400				  (T(SETQ NA(CONS NA(READ)))))
03450			     (COND((THVAL @(THNOT(THGOAL(THEV NA)))THALIST)(THVAL @(THASSERT(THEV NA))THALIST))))))
03500		     (T(COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
03550			    (T(SETQ NA(CONS NA(READ)))))
03600		       (COND((THVAL @(THGOAL(THEV NA))THALIST)(THVAL @(THERASE(THEV NA))THALIST))))  )
03650	
03700		(SETQ AL(CONS(REVERSE(CONS NA ADV))AL))
03750		(GO AD01)
03800	AD3	(SETQ NA(READ))
03850		(COND((NOT(OR(GET NA @DEF)(AND(EQ NEGSGN(CAR(EXPLODE NA)))(GET(READLIST(CDR(EXPLODE NA)))@DEF))))
03900		      (SETQ AL(CONS(REVERSE(CONS NA ADV))AL))(GO AD02)))
03950		(COND((EQ NEGSGN(CAR(EXPLODE NA)))
04000		      (COND((GET(READLIST(CDR(EXPLODE NA)))@PARTIAL)(SETQ NA(READLIST(APPEND @(N)(CDR(EXPLODE NA)))))
04050			    (COND((GET(READLIST(CDR(EXPLODE NA)))@FLUENT)
04100				  (SETQ NA(CONS NA(APPEND(READ)@(R)))))
04150				 (T(SETQ NA(CONS NA(READ)))))
04200			    (COND((THVAL @(THNOT(THGOAL(THEV NA)))THALIST)(THVAL @(THASSERT(THEV NA))THALIST))))
04250			   (T(SETQ NA(READLIST(CDR(EXPLODE NA))))
04300			     (COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
04350				  (T(SETQ NA(CONS NA(READ)))))
04400			     (COND((THVAL @(THGOAL(THEV NA))THALIST)(THVAL @(THERASE(THEV NA))THALIST))))))
04450		     (T(COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
04500			    (T(SETQ NA(CONS NA(READ)))))
04550		       (COND((THVAL @(THNOT(THGOAL(THEV NA)))THALIST)(THVAL @(THASSERT(THEV NA))THALIST))))  )
04600		(SETQ AL(CONS(REVERSE(CONS NA ADV))AL))
04650		(GO AD01)
04700	AD4	(SETQ NA(READ))
04750		(COND((NOT(GET NA @THEOREM))(PRINT NA)(PRINC @_IS_NOT_DEFINED)
04800		      (SETQ AN(SUB1 AN))(GO AD01)))
04850		(SETQ AL(CONS(REVERSE(CONS(GET NA @THEOREM)(CONS NA ADV)))AL))
04900		(THVAL @(THERASE(THEV NA))THALIST)
04950		(REMPROP NA @THEOREM)
05000		(GO AD02)
05050	AD5	(SETQ NA(READ))
05100		(COND((NOT(OR(GET NA @DEF)(AND(EQ NEGSGN(CAR(EXPLODE NA)))(GET(READLIST(CDR(EXPLODE NA)))@DEF))))
05150		      (SETQ AL(CONS(REVERSE(CONS NA ADV))AL))(GO AD02)))
05200		(COND((EQ NEGSGN(CAR(EXPLODE NA)))
05250		      (COND((GET(READLIST(CDR(EXPLODE NA)))@PARTIAL)(SETQ NA(READLIST(APPEND @(N)(CDR(EXPLODE NA)))))
05300			    (COND((GET(READLIST(CDR(EXPLODE NA)))@FLUENT)
05350				  (SETQ NA(CONS NA(APPEND(READ)@(R)))))
05400				 (T(SETQ NA(CONS NA(READ)))))  )
05450			   (T(SETQ NA(READLIST(CDR(EXPLODE NA))))
05500			     (COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
05550				  (T(SETQ NA(CONS NA(READ)))))
05600			     (COND((THVAL @(THGOAL(THEV NA))THALIST)(THVAL @(THERASE(THEV NA))THALIST))))))
05650		     (T(COND((GET NA @FLUENT)(SETQ NA(CONS NA(APPEND(READ)@(R)))))
05700			    (T(SETQ NA(CONS NA(READ))))) ) )
05750		(SETQ OPT(READLIST(APPEND @(T)(EXPLODE(CAR NA)))))
05800		(PUTPROP OPT(LIST @THCONSE(PTHV(CDR NA))(CONS(CAR NA)(CDR NA))
05850				  (LIST @THSETQ @(THV ASSL)(LIST @CONS NA @(THV ASSL))))
05900			    @THEOREM)
05950		(THASSERT(THEV OPT))
06000		(SETQ AL(CONS(REVERSE(CONS OPT ADV))AL))
06050		(GO AD01)
06100	AD6	(SETQ ADV(CONS(READ)ADV))
06150		(SETQ NA(CAR ADV))
06200		(COND((NOT(GET NA @THEOREM))(PRINT NA)(PRINC @_IS_NOT_DEFINED)(SETQ AN(SUB1 AN))(GO AD01)))
06250		(SETQ OPT(READ))
06300		(SETQ ADV(CONS OPT ADV))
06350		(SETQ ADV(CONS(READ)ADV))
06400		(COND((EQ OPT @TO)(SET(READLIST(APPEND @(R T)(EXPLODE NA)))
06450				      (APPEND(CAR ADV)(EVAL(READLIST(APPEND @(R T)(EXPLODE NA)))))))
06500		     ((EQ OPT @FROM)(SET(READLIST(APPEND @(R F)(EXPLODE NA)))
06550				        (APPEND(CAR ADV)(EVAL(READLIST(APPEND @(R F)(EXPLODE NA)))))))
06600		     (T(PRINT OPT)(PRINC @_IS_NOT_A_VALID_OPTION)(SETQ AN(SUB1 AN))(GO AD01)))
06650		(SETQ AL(CONS(REVERSE ADV)AL))
06700		(GO AD01)
06750	AD7	(SETQ AN(SUB1 AN))
06800		(TERPRI)(TERPRI)
06850		(COND((NULL AL)(PRINT @NO_ADVICE_GIVEN_THIS_SESSION)(GO AD01)))
06900		(PRINT @**_ADVICE_GIVEN_DURING_THIS_SESSION_**)
06950		(TERPRI)
07000		(SETQ ALR(REVERSE AL))
07050	AD03	(COND((NULL ALR)(GO AD01)))
07100		(COND((EQ @ALTER(CADAR ALR))(GO AD05)))
07150		(PRINT(CAR ALR))
07200		(SETQ ALR(CDR ALR))   (GO AD03)
07250	AD05	(PRINT(LIST(CAAR ALR)(CADAR ALR)(CADDAR ALR)))
07300		(PRINT @DO_YOU_WANT_TO_SEE_PREVIOUS_VERSION?*)
07350		(COND((READ)(SPRINT(CADR(CDDAR ALR))2 2)))
07400		(PRINT @DO_YOU_WANT_TO_SEE_THE_PRESENT_VERSION?*)
07450		(COND((READ)(SPRINT(GET(CADDAR ALR)@THEOREM)2 2)))
07500		(SETQ ALR(CDR ALR))
07550		(GO AD03) 
07600	AD8	(SETQ AN(SUB1 AN))
07650		(TERPRI)(TERPRI)
07700		(PRINT @RULES_ENTERED_AND_GOALS_PENDING_IN_CURRENT_SUBGOAL_TREE_PATH:)
07750		(PRINT @___)(PRTRULES CT ) 
07800		(TERPRI)
07850		(PRINT @CURRENT_PLAN:)
07900		(TSLPLAN(REVERSE(EVAL(CAR(THV ANS)))))
07950		(TERPRI)
08000		(PRINT @RULES_AND_GOALS_IN_LONGEST_PATH_OBTAINED_THUS_FAR:)
08050		(PRINT @___)(PRTRULES LCT) 
08100		(TERPRI)
08150		(PRINT @LONGEST_PLAN:)
08200		(TSLPLAN LGANS)
08250		(TERPRI)
08300		(GO AD01)  ))
08350	EXPR)
08400	
08450	
08500	
08550	
08600	
08650	
08700	
08750	(DEFPROP PRTRULES
08800	   (LAMBDA(X)
08850	      (PROG(TEM)
08900		(COND((NULL X)(RETURN NIL)))
08950		(SETQ TEM(REVERSE X))
09000	PRT2	(PRINC(CAAR TEM))
09050		(SETQ TEM(CDR TEM))
09100		(COND(TEM(GO PRT2))) ))
09150	EXPR)
09200	
09250	
09300	(DEFPROP PTHV
09350	   (LAMBDA(ARL)
09400	λαSOND((NULL ARL)NIL)
09450		     ((ATOM(CAR ARL))(PTHV(CDR ARL)))
09500		     (T(APPEND(LIST(CADAR ARL))(PTHV(CDR ARL))))))
09550	EXPR)
09600	
09650	
09700	
09750	(DEFPROP TREEPATH
09800	   (LAMBDA(OP)
09850	      (PROG NIL
09900		(SETQ CT (CONS(LIST(CAR OP))CT ))
09950		(THSETQ (THV CGL)(THVARSUBST(CADR OP)))
10000		(COND((*GREAT(LENGTH CT )(LENGTH LCT))
10050		      (SETQ LCT CT )))
10100		(RETURN T)))
10150	FEXPR)
10200	
10250	
10300	(DEFPROP TRACEINFO1
10350	   (LAMBDA NIL
10400	      (PROG NIL
10450		(PRINT @RULES_ENTERED_AND_GOALS_PENDING_IN_CURRENT_SUBGOAL_TREE_PATH:)
10500		(PRINT @___)
10550		(PRTRULES CT )       
10600		(TERPRI)
10650		(RETURN T) ))
10700	EXPR)
10750	
10800	
10850	
10900	(DEFPROP TRACEINFO2
10950	   (LAMBDA (OP)
11000	      (PROG NIL
11050		(PRINT(CAR OP))(PRINC @_IS_FAILING!!!!)
11100		(COND((NOT(ATOM(CAAR CT )))
11150		      (PRINT @___)(PRINC(CADAAR CT ))
11200		      (PRINC @_WAS_THE_LOSER) ))
11250		(TERPRI)
11300		(COND((AND(TTYIN)(ADVICESYS))(RETURN T)))
11350		(SETQ CT(CDR CT))
11400		(RETURN NIL) ))
11450	FEXPR)
11500	
11550	
11600	
11650	(DEFPROP DELAD1
11700	   (LAMBDA(NU L)
11800		(COND((NULL L)NIL)
11850		     ((EQ NU(CAAR L))(DELAD1 NU(CDR L)))
11900		     (T(CONS(CAR L)(DELAD1 NU(CDR L))))))
12000	EXPR)
12050	
12100	
12150	(DEFPROP DELRL
12200	   (LAMBDA(RL EL)
12250	(PROG NIL (PRINT RL)(PRINT EL)
12300		(COND((NULL RL)NIL)
12350		     ((MEMQ(CAR RL)EL)(DELRL(CDR RL)EL))
12400		     (T(CONS(CAR RL)(DELRL(CDR RL)EL)))))
12450	)
12500	EXPR)
12550	
12600	
12650	(DEFPROP DELAD
12700	   (LAMBDA(NUM)
12750	      (PROG(AD TE)
12800	(PRINT @L1825)(PRINT NUM)
12850		(SETQ AN(SUB1 AN))
12900		(SETQ AD(ASSOC(READLIST(CDR(EXPLODE NUM)))AL))
12950		(COND((NULL AD)(PRINT @NO_SUCH_ADVICE_GIVEN)(RETURN T)))
13000		(SETQ AL(DELAD1(READLIST(CDR(EXPLODE NUM)))AL))
13050	(PRINT @L1841)(PRINT AD)(PRINT AL)
13100		(SETQ AD(CDR AD))
13150		(GO(CDR(ASSOC(CAR AD)@((FOR . DE1)(DELETE . DE2)(ADD . DE3)(ALTER . DE4)(ASSUME . DE5)(RESTRICT . DE6)))))
13200	DE1	(SETQ AD(CDR AD))
13250		(COND((EQ @FIRST(CADR AD))
13300		      (RPLACD(FBODY(GET(CAR AD)@THEOREM))
13350			     (CDDR(FBODY(GET(CAR AD)@THEOREM)))))
13400		     (T(RPLACD(FBODY(GET(CAR AD)@THEOREM))
13450			      (CDADDR(FBODY(GET(CAR AD)@THEOREM))))))
13500		(RETURN T)
13550	DE2	(THVAL @(THASSERT(THEV(CADR AD)))THALIST)
13600		(RETURN T)
13650	DE3	(THVAL @(THERASE(THEV(CADR AD)))THALIST)
13700		(RETURN T)
13750	DE4	(THVAL @(THERASE(THEV(CADR AD)))THALIST)
13800		(REMPROP(CADR AD)@THEOREM)
13850		(PUTPROP(CADR AD)(CADDR AD)@THEOREM)
13900		(THVAL @(THASSERT(THEV(CADR AD)))THALIST)
13950		(RETURN T)
14000	DE5	(THVAL @(THERASE(THEV(CADR AD)))THALIST)
14050		(RETURN T)
14100	DE6	(SETQ TE(COND((EQ(CADDR AD)@TO)(READLIST(APPEND @(R T)(EXPLODE(CADR AD)))))
14150			     (T(READLIST(APPEND @(R F)(EXPLODE(CADR AD)))))))
14200		(SET TE(DELRL(EVAL TE)(CADDDR AD)))
14250		(RETURN T)   ))
14300	EXPR)
14350	
14400	
14410	
14420	(DEFPROP FILTERAX
14430	   (LAMBDA(THM)
14440		(GET THM @AX)  )
14445	EXPR)
14450	
14500	(DEFPROP FILTEROP
14550	   (LAMBDA(THM)
14600		(AND  
14650		   (OR(NOT(GET(CAAAR CT )@AX))(GET THM @AX))
14700		   (OR(GET(CAAAR CT )@REC)(NOT(EQ(CAAAR CT )THM)))
14750		   (OR(NULL(EVAL(READLIST(APPEND @(R T)(EXPLODE(CAAAR CT ))))))
14800		      (MEMQ THM(EVAL(READLIST(APPEND @(R T)(EXPLODE(CAAAR CT )))))))
14850		   (OR(NULL(EVAL(READLIST(APPEND @(R F)(EXPLODE(CAAAR CT ))))))
14900		      (NOT(MEMQ THM(EVAL(READLIST(APPEND @(R F)(EXPLODE(CAAAR CT ))))))))  ) )
14950	EXPR)
15000	
15050	
15100	
15150	
15200	(DEFPROP FBODY
15250	   (LAMBDA(B)
15300		(COND((OR(EQ(CAAR(CDDDR B))@THGOAL)(AND(EQ(CAAR(CDDDR B))@THOR)
15350							(EQ(CAADAR(CDDDR B))@THAND)))
15400		      (CDDR B))
15450		     (T(FBODY(CDR B))))   )
15500	EXPR)
15550	
15600	
15650	
15700	(DEFPROP OPTIM
15750	   (LAMBDA(PLN)
15800	      (PROG(OPLN SUL)
15850		(SETQ OPLN(OPDEAD PLN PLN))
15900		
15950	
16000	OP3	(COND((NULL SUL)(RETURN OPLN)))				
16050		(SETQ OPLN(SUBST(CAAR SUL)(CDAR SUL)OPLN))
16100		(SETQ GOL(SUBST(CAAR SUL)(CDAR SUL)GOL))
16150		(SETQ SUL(CDR SUL))
16200		(GO OP3)      ))
16250	EXPR)
16300	
16350	
16400	(DEFPROP OPDEAD
16450	   (LAMBDA(PLNA PLN)
16500		(COND((ATOM PLNA)PLNA)
16550		     ((AND(EQ @←(CAR PLNA))(NOT(XRH(CADR PLNA)PLN))(NOT(XNA(CADR PLNA)PLN))
16600			  (COND((ATOM(CADDR PLNA))(SETQ SUL(CONS(CONS(CADDR PLNA)(CADR PLNA))SUL)))
16650			       (T T))   )
16700		      NIL)
16750		     (T(APPEND(CLIST(OPDEAD(CAR PLNA)PLN))(OPDEAD(CDR PLNA)PLN))))  )
16800	EXPR)
16850	
16900	
16950	(DEFPROP CLIST
17000	   (LAMBDA(X)
17050		(COND((NULL X)NIL)
17100		     (T(LIST X))))
17150	EXPR)
17200	
17250	
17300	(DEFPROP XRH
17350	   (LAMBDA(X P)
17400		(COND((ATOM P)NIL)
17450		     ((EQ @←(CAR P))(SUBSTP(CADDR P)X))
17500		     (T(OR(XRH X(CAR P))(XRH X(CDR P))))))
17550	EXPR)
17600	
17650	
17700	(DEFPROP XNA
17750	   (LAMBDA(X P)
17800		(COND((EQ X P)T)
17850		     ((ATOM P)NIL)
17900		     ((EQ @←(CAR P))NIL)
17950		     (T(OR(XNA X(CAR P))(XNA X(CDR P))))))
18000	EXPR)
18050	
18100	(DEFPROP TSLPLAN
18150	   (LAMBDA(P)
18200	      (PROG(PL SEMCOL)
18250		(SETQ PL P)
18300		(COND((NULL PL)(RETURN NIL)))
18350		(SETQ INDENT(CONS @"   " INDENT))
18400		(TERPRI)
18450		(PRINDENT INDENT)
18500		(PRINC @BEGIN)(TERPRI)
18550	T1	(PRINDENT INDENT)
18600		(TSLPLANI(CAR PL))
18650		(SETQ PL(CDR PL))
18700		(COND((NOT(NULL PL))(GO T1)))
18750		(PRINDENT INDENT)
18800		(PRINC @END)(TERPRI)
18850		(SETQ INDENT(CDR INDENT))
18900		(RETURN T)  )) 
18950	EXPR)
19000	
19050	
19100	(DEFPROP TSLPLANI
19150	   (LAMBDA(PI)
19200	      (PROG(PIT)
19250		(SETQ PIT PI)
19300		(COND((EQ(CAR PIT)@IF)(GO TS3))
19350		     ((EQ(CAR PIT)@WHILE)(GO TS6))
19400		     ((EQ(CAR PIT)@←)(GO TS9)) )
19450		(PRINC(CAR PIT))
19500		(COND((NULL(CDR PIT))(PRINC @;)(TERPRI)(RETURN T)))
19550		(PRINC(CDR PIT))
19600		(GO TS13)
19650	TS3	(SETQ PIT(CDR PIT))
19700		(PRINC @"IF ")
19750		(TSTCOND(CAR PIT))
19800		(SETQ PIT(CDR PIT))
19850		(PRINC @" THEN ")
19900		(SETQ PIT(CDR PIT))
19950		(COND((CDR PIT)(SETQ SEMCOL T)))
20000		(SETQ INDENT(CONS @"   " INDENT))
20050		(TERPRI)   (PRINDENT INDENT)
20100		(TSLPLANI(CAR PIT))
20150		(SETQ PIT(CDR PIT))
20200		(SETQ INDENT(CDR INDENT))
20250		(COND((NULL PIT)(RETURN T)))
20300		(SETQ PIT(CDR PIT))
20350		(PRINDENT INDENT)
20400		(PRINC @"ELSE ")
20450		(COND((AND(ATOM(CAAR PIT))(NOT SEMCOL))(TSLPLANI(CAR PIT))(GO TS13))
20500		     ((ATOM(CAAR PIT))(TSLPLANI(CAR PIT))(RETURN T))
20550		     (T(TSLPLAN(CAR PIT))(RETURN T)))
20600	TS6	(SETQ PIT(CDR PIT))
20650		(PRINC @"WHILE ")
20700		(TSTCOND(CAR PIT))
20750		(SETQ PIT(CDDR PIT))
20800		(PRINC @" DO ")
20850		(TSLPLAN(CAR PIT))
20900		(RETURN T)
20950	TS9	(SETQ PIT(CDR PIT))
21000		(PRINC(CAR PIT))
21050		(PRINC @" ← ")
21100		(SETQ PIT(CDR PIT))
21150		(COND((ATOM(CAR PIT))(GO TS11)))
21200		(COND((NOT(FUNDEF(CAR PIT)T))(GO TS13)))
21250		(PRINC(CAAR PIT))
21300		(COND((NULL(CDAR PIT))(GO TS13)))
21350		(COND((ATOM(CADAR PIT))(PRINC(CDAR PIT)))
21400		     (T(PRINC(CADAR PIT))))
21450		(GO TS13)
21500	TS11	(PRINC(CAR PIT))
21550	TS13	(COND((NOT SEMCOL)(PRINC @;))) (TERPRI)
21600		(RETURN T) ))
21650	EXPR)
21700	
21750	
21800	(DEFPROP FUNDEF
21850	   (LAMBDA(FU SW)
21900	      (PROG(FFL FAL AAL EAAL)
21950		(SETQ FFL(ASSOC(CAR FU)FUNDEFLIST))
22000		(COND((NULL FFL)(RETURN FU)))
22050		(SETQ FAL(CADR FFL))
22100		(SETQ FFL(CADDR FFL))
22150		(SETQ AAL(CDR FU))
22200	FU3	(COND((ATOM(CAR AAL))(SETQ EAAL(CAR AAL)))
22250		     (T(SETQ EAAL(FUNDEF(CAR AAL)NIL))))
22300		(SETQ FFL(SUBST EAAL (CAR FAL)FFL))
22350		(SETQ AAL(CDR AAL))
22400		(SETQ FAL(CDR FAL))
22450		(COND(FAL(GO FU3)))
22500		(COND(SW(MAPC(FUNCTION NPRINC)FFL))
22550		     (T(RETURN FFL)))
22600		(RETURN NIL)  ))
22650	EXPR)
22700	
22750	
22800	
22850	(DEFPROP NPRINC
22900	   (LAMBDA(FF)
22950		(COND((ATOM FF)(PRINC FF))
23000		     (T(MAPC(FUNCTION NPRINC)FF)))  )
23050	EXPR)
23100	
23150	
23200	(DEFPROP PRINDENT
23250	   (LAMBDA(I)
23300	      (PROG(II)
23350		(SETQ II I)
23400	PR4	(PRINC(CAR II))
23450		(SETQ II(CDR II))
23500		(COND((NULL II)(RETURN T))
23550		     (T(GO PR4)))  ))
23600	EXPR)
23650	
23700	
23750	(DEFPROP TSTCOND
23800	   (LAMBDA(C)
23850	      (PROG(CC CC1)
23900		(SETQ CC C)
23910	TS0     (COND((ATOM(CAR C))(SETQ CC1 CC))
23914	             (T(SETQ CC1(CAR CC))))
23950		(COND((NOT(EQ NEGSGN(CAR CC1)))(GO TS2)))
24000		(PRINC NEGSGN)
24050		(SETQ CC1(CDR CC1))
24100	TS2	(PRINC(CAR CC1))
24150		(PRINC(CDR CC1)) 
24160	        (SETQ CC(CDR CC))
24164	        (COND((OR(ATOM(CAR C))(NULL CC))(RETURN T)))
24168	        (PRINC @"  ")(PRINC @∧)(PRINC @"  ")
24172	        (GO TS0)  ))
24200	EXPR)
24250	
24300	(DEFPROP UNCERTLIT
24350	   (LAMBDA(LI DSW LI1 LI2)
24400	      (PROG NIL
24450		(SETQ UNCERTLIST(APPEND UNCERTLIST(LIST LI)))
24500		(RPLACA CT(CONS(CAAR CT)(UPDATLIT(CDAR CT)LI1 @X)))
24550		(RPLACA CT(CONS(CAAR CT)(UPDATLIT(CDAR CT)LI2 @X)))
24600		(COND(DSW(RETURN NIL))
24650		     (T(RETURN T)))  ))
24700	EXPR)
24750	
24800	(DEFPROP FINDINSTANG
24850	   (LAMBDA(CTH)
24900		(COND((NULL CTH)NIL)
24950		     ((NULL(CDR CTH))(RPLACA CTH(CONS(CAAR CTH)(CONS @IF(CDAR CTH))))GOL)
25000		     ((NOT(SUBSTP(CAR(CDAADR CTH))@THV))
25050		      (RPLACA CTH(CONS(CAAR CTH)(CONS @IF(CDAR CTH))))
25100		      (CAR(CDAADR CTH)))
25150		     (T(FINDINSTANG(CDR CTH))))   )
25200	EXPR)
25250	
25300	(DEFPROP CONDSTAT
25350	   (LAMBDA(G DSW)
25400	      (PROG (TE GL PRLIST)
25450		(COND((AND(NULL UNCERTLIST)DSW)(RETURN NIL))
25500		     ((NULL UNCERTLIST)(RETURN T)))
25550		(COND((NOT(SUBSTP G @THV))(SETQ GL G)(RPLACA CT(CONS(CAAR CT)(CONS @IF(CDAR CT)))))
25600		     (T(SETQ GL(FINDINSTANG CT))))
25650		(SETQ SSW T)
25700	         (SETQ TE(CONS(APPEND(LIST @IF(TSTLIT2(CAR UNCERTLIST)) @THEN)
25850				    (LIST(NESTIF(LIST(CAR UNCERTLIST))(CDR UNCERTLIST)GL))@(ELSE))(EVAL(CAR(THV ANS)))))
25900		(THSET(CAR(THV ANS))TE)
25950		(THASSERT(THEV(CAR UNCERTLIST)))
25975		(THSETQ(THV PASSUM)(CONS(CAR UNCERTLIST)(THV PASSUM)))
26000		(SETQ UNCERTLIST NIL)
26050		(THSETQ(THV PROCLIST)(CONS PRLIST(THV PROCLIST)))
26100		(THSETQ(THV ANS)(CONS(LIST @THV(GENSYM))(THV ANS)))
26150		(THVSET(CAR(THV ANS))NIL)
26200		(SETQ SSW NIL)
26250		(RETURN T)  ))
26300	EXPR)
26350	
26400	
26450	(DEFPROP NESTIF
26500	   (LAMBDA(FL TL GL)
26550		(COND((NULL TL)(PROCALL FL TL GL))
26600	             (T(APPEND(LIST @IF(TSTLIT2(CAR TL))@THEN)
26750			      (LIST(NESTIF(CONS(CAR TL)FL)(CDR TL)GL))
26800			      (LIST @ELSE (PROCALL FL TL GL))))))
26850	EXPR)
26900	
26950	
27000	(DEFPROP PROCALL
27050	   (LAMBDA(FL TL GL)
27100	      (PROG(PL ST PFL LI QFL)
27150		(SETQ PFL FL)
27200		(SETQ PL(READLIST(APPEND @(P R O C)(EXPLODE(SETQ PN(ADD1 PN))))))
27250		(SETQ PRLIST(CONS PL PRLIST))
27300		(SETQ ST(CONS(READLIST(APPEND @(S T A T)(EXPLODE(SETQ SN(ADD1 SN)))))@CST))
27350		(COND(TL(THVAL @(THASSERT(THEV(CAR TL)))THALIST)))
27400	PR2	(SETQ LI(CAR PFL))
27450		(COND((EQ @N(CAR(EXPLODE(CAR LI))))
27500		      (SETQ LI(CONS(READLIST(CDR(EXPLODE(CAR LI))))(CDR LI))))
27550		     (T(SETQ LI(CONS(READLIST(CONS @N(EXPLODE(CAR LI))))(CDR LI)))))
27600		(SETQ QFL(CONS LI QFL))
27650		(THASSERT(THEV LI))
27700		(SETQ PFL(CDR PFL))
27750		(COND(PFL(GO PR2)))
27800		(EVAL(LIST @OUTC(LIST @OUTPUT @DSK: ST)T))
27850		(THDUMP)
27900		(OUTC NIL)
27950	PR4	(THERASE(THEV(CAR QFL)))
28000		(SETQ QFL(CDR QFL))
28050		(COND(QFL(GO PR4)))
28100		(COND(TL(THVAL @(THERASE(THEV(CAR TL)))THALIST)))
28150		(SETQ FIFOL(APPEND FIFOL(LIST(LIST PL GL ST))))
28160	        (THSETQ(THV COMMENTLIST)(CONS(LIST  PL @ATTEMPTS_TO_ACHIEVE_
28162						   (TSTLIT GL))(THV COMMENTLIST)))
28200		(RETURN(APPEND(LIST PL)(CDR(TSTLIT GL))))  ))
28250	EXPR)
28300	
28350	(DEFPROP INSTANTHV
28400	   (LAMBDA(LL)
28450		(COND((NULL LL)NIL)
28500		     ((ATOM LL)LL)
28550		     ((EQ(CAR LL)@THV)(THVAL LL THALIST))
28600		     (T(CONS(INSTANTHV(CAR LL))(INSTANTHV(CDR LL))))))
28650	EXPR)
28700	
28750	
28800	(DEFPROP DISPOST
28850	   (LAMBDA(DNF)
28900	      (PROG(TE PRLIST)
28950		(SETQ SSW T)
29000		(SETQ DNF(INSTANTHV DNF))
29050		(SETQ TE(CONS(APPEND(LIST @IF(NRTSTLITS(PTESTLITS(CADR DNF)(APPEND(CDDR DNF)(LIST(CAR DNF)))))@THEN)
29100				    (LIST(NESTIFP(LIST(CAR DNF))(CDR DNF)(CAAR DNF))))
29150			     (EVAL(CAR(THV ANS)))))
29200		(THSET(CAR(THV ANS))TE)
29250		(THSETQ(THV PROCDATA)(CONS(LIST PRLIST(THV DBLITS)(THV ASSERTLITS))
29300					  (THV PROCDATA)))
29350		(SETQ SSW NIL)
29400		(RETURN T)   ))
29450	EXPR)
29500	
29550	
29600	(DEFPROP NESTIFP
29650	   (LAMBDA(ADF DF GLP)
29700		(COND((NULL(CDR  DF))(PROCALLP(APPEND DF ADF) GLP))
29750		     (T(APPEND(LIST @IF(NRTSTLITS(PTESTLITS(CADR DF)(APPEND(CDDR DF)(CONS(CAR DF)ADF))))@THEN)
29800			      (LIST(NESTIFP(CONS(CAR DF)ADF)(CDR DF)GLP))
29850			      (LIST @ELSE(PROCALLP (APPEND DF ADF) GLP)))))   )
29900	EXPR)
29950	
30000	
30050	(DEFPROP TSTLIT
30100	   (LAMBDA(LI)
30150		(COND((EQ @R(CAR(LAST LI)))(REVERSE(CDR(REVERSE LI))))
30200		     (T LI))   )
30250	EXPR)
30300	
30350	
30400	(DEFPROP PROCALLP
30450	   (LAMBDA(DF GLP)
30500	      (PROG(PL ST CL SSW CLL)
30510	         (SETQ CLL DF)
30550		(SETQ PL(READLIST(APPEND @(P R O C)(EXPLODE(SETQ PN(ADD1 PN))))))
30600		(SETQ PRLIST(CONS PL PRLIST))
30650		(SETQ ST(CONS(READLIST(APPEND @(S T A T)(EXPLODE(SETQ SN(ADD1 SN)))))@CST))
30700		(SAVESTATE @XXXX)
30750		(THFLUSH THASSERTION THERASING THCONSE)
30800		(DSKIN CURSTATE)
30850		(COND((NULL DF)(GO PR7)))
30900	PR1      (SETQ CL(CAR CLL))
30910	PR3      (ASSERTPOST(CAR CL)SSW)
30920	         (SETQ CL(CDR CL))
30930	         (COND(CL(GO PR3)))
30940	         (SETQ SSW T)
30950	         (SETQ CLL(CDR CLL))
30960	         (COND(CLL(GO PR1)))
31100	PR7	(EVAL(LIST @OUTC(LIST @OUTPUT @DSK: ST)T))
31150		(THDUMP)(OUTC NIL)
31200		(SETQ FIFOL(APPEND FIFOL(LIST(LIST PL GLP ST))))
31250		(THFLUSH THASSERTION THERASING THCONSE)
31300		(DSKIN XXXX)
31310		(THSETQ(THV COMMENTLIST)(CONS(LIST  PL @ATTEMPTS_TO_ACHIEVE_
31312						   (TSTLIT GLP))(THV COMMENTLIST)))
31350		(RETURN(APPEND(LIST PL)(CDR(TSTLIT GLP))))   ))
31400	EXPR)
31450	
31500	
31550	(DEFPROP SAVESTATE
31600	   (LAMBDA(SS)
31650	      (PROG  NIL
31700		(EVAL(LIST @OUTC(LIST @OUTPUT @DSK: SS)T))
31750		(THDUMP)
31800		(OUTC NIL)   (RETURN T)  ))
31850	EXPR)
31900	
31910	(DEFPROP TSTLIT2
31913	   (LAMBDA(LI)
31916	      (PROG(LIT)
31919	        (COND((EQ @R(CAR(LAST LI)))
31922	              (SETQ LIT(REVERSE(CDR(REVERSE LI))))))
31925	        (COND((EQ NEGSGN(CAR LI))
31928	              (SETQ LIT(CDR LIT)))
31931	             ((EQ @N(CAR(EXPLODE(CAR LI))))
31934	              (SETQ LIT(CONS(READLIST(CDR(EXPLODE(CAR LI))))(CDR  LIT))))
31937	             (T(SETQ LIT(CONS NEGSGN LIT))))
31940	        (RETURN LIT)  ))
31943	EXPR)
31946	
31949	
31950	(DEFPROP PTESTLITS
31953	   (LAMBDA(PO NEG)
31956	        (COND((NULL NEG)(LIST(TSTLIT(CAR PO))))
31959	             (T(CONS(TSTLIT2(CAAR NEG))(PTESTLITS PO(CDR NEG))))))
31962	EXPR)
31965	
31968	
31971	(DEFPROP NRTSTLITS
31974	   (LAMBDA(LL)
31977	        (COND((MEMBER(CAR(LAST LL))(CDR(REVERSE LL)))
31980	              (CDR(REVERSE LL)))
31983	             (T(REVERSE LL))))
31986	EXPR)
31989	
31992	
31995	(DEFPROP ASSERTPOST
31998	   (LAMBDA(LI SW)
32001	      (PROG(NSW LIT PSW)
32004	        (COND((EQ @N(CAR(EXPLODE(CAR LI))))
32007	              (SETQ LIT(CONS(READLIST(CDR(EXPLODE(CAR LI))))(CDR  LI)))
32010	              (SETQ NSW T))
32013	             (T(SETQ LIT LI)))
32016	        (COND((GET(CAR LIT)@PARTIAL)(SETQ PSW T)))
32019	        (COND((OR(AND NSW PSW(NOT SW))
32022	                 (AND(NOT NSW)PSW(NOT SW))
32025	                 (AND(NOT NSW)(NOT PSW)(NOT SW))
32028	                 (AND NSW(NOT PSW)SW))
32031	              (THASSERT(THEV(CONS(READLIST(CONS @N(EXPLODE(CAR LI))))(CDR LI))))))
32034	        (RETURN T)   ))
32037	EXPR)
32040	
32043	
32050	
32100	
32150	(DEFPROP ELSECLAUSE
32200	   (LAMBDA NIL
32250	      (PROG(CB IFS)
32300		(SETQ IFS(CDAR CT))
32350		(THSETQ CT(CDR CT)T T)
32400	EL2	(SETQ CB(REVERSE(EVAL(CAR(THV ANS)))))
32450		(THSETQ(THV ANS)(CDR(THV ANS)))
32500		(THSET(CAR(THV ANS))(CONS(APPEND(CAR(EVAL(CAR(THV ANS))))
32550						(LIST CB))
32600					 (CDR(EVAL(CAR(THV ANS)))))  )
32650		(SETQ GANS(REVERSE(EVAL(CAR(THV ANS)))))
32700		(THSETQ(THV PROCDATA)(CONS(LIST(CAR(THV PROCLIST))(THV DBLITS)(THV ASSERTLITS))
32750					  (THV PROCDATA)))
32800		(THSETQ(THV PROCLIST)(CDR(THV PROCLIST))T T)
32850		(SETQ IFS(CDR IFS))
32900		(COND((ATOM(CAR IFS))(GO EL2)))
32950		(RETURN T)   ))
33000	EXPR)
33050	
35600	
35650	
35700	(DEFPROP SUBPLANL
35750	   (LAMBDA(P PL)
35800		(COND((NULL PL)P)
35850		     (T(SUBPLANL(SUBPLANL1 P(CAR PL))(CDR PL)))))
35900	EXPR)
35950	
36000	
36050	(DEFPROP SUBPLANL1
36100	   (LAMBDA(P PL)
36150		(COND((ATOM P)P)
36200		     ((AND(NOT(ATOM(CAR P)))(EQ @←(CAAR P))(EQ(CAADDR(CAR   P))(CAAR PL)))
36250	              (SUBPLANL1(APPEND(REVERSE(SUBPLANL2(CAR P)PL))(CDR P))PL))
36300		     (T(CONS(SUBPLANL1(CAR P)PL)(SUBPLANL1(CDR P)PL)))))
36350	EXPR)
36400	
36450	
36500	(DEFPROP SUBPLANL2
36550	   (LAMBDA(P PL)
36600	      (PROG(PT PLT BOD)
36625	(PRINT @L36625)(PRINT P)(PRINT PL)
36650		(SETQ PT P)(SETQ PLT PL)
36700		(SETQ BOD(CADR PLT))
36750		(SETQ BOD(SUBST(CADR PT)(CADAR PLT)BOD))
36800		(SETQ PT(CDADDR PT))
36850		(SETQ PLT(CDDAR PLT))
36900	SU2	(COND((NULL PT)(RETURN BOD)))
36950		(SETQ BOD(SUBST(CAR PT)(CAR PLT)BOD))
37000		(SETQ PT(CDR PT))
37050		(SETQ PLT(CDR PLT))
37100		(GO SU2)   ))
37150	EXPR)
37160	
37163	(DEFPROP DELL
37166	   (LAMBDA(C L)
37169		(COND((NULL L)NIL)
37172		     ((AND(CDDR C)(CDDAR L)(EQUAL(CAR C)(CAAR L))
37175			  (EQUAL(CADR C)(CADAR L))
37178			  (COND((CADDR C)(EQUAL(CADDR C)(CADDAR L)))
37181			       (T T)))
37184		      (CDR L))
37187		     ((AND(NULL(CDDR C))(NULL(CDDAR L))(EQUAL(CAR C)(CAAR L))
37190			  (COND((CADR C)(EQUAL(CADR C)(CADAR L)))
37193			       (T T)))
37196		      (CDR L))
37199		     (T(CONS(CAR L)(DELL C(CDR L)))))  )
37202	EXPR)
37205	
37208	
37211	(DEFPROP FINDC
37214	   (LAMBDA(C L)
37217		(COND((NULL L)NIL)
37220		     ((AND(CDDR C)(CDDAR L)(EQUAL(CAR C)(CAAR L))
37223			  (EQUAL(CADR C)(CADAR L))
37226			  (COND((CADDR C)(EQUAL(CADDR C)(CADDAR L)))
37229			       (T T)))
37232		      (CAR L))
37235		     ((AND(NULL(CDDR C))(NULL(CDDAR L))(EQUAL(CAR C)(CAAR L))
37238			  (COND((CADR C)(EQUAL(CADR C)(CADAR L1)))
37241			       (T T)))
37244		      (CAR L))
37247		     (T(FINDC C(CDR L))))  )
37250	EXPR)
37253	
37255	(DEFPROP ELEVA
37257	   (LAMBDA(C L)
37259		(COND((NULL L)NIL)
37261		     ((AND(NULL(CDDAR L))(EQUAL(CAAR C)(CADAAR L)))
37263		      (SETQ SW T)(CONS(LIST(CAAR L)(NRCONJ(CADAR L)(CADR C)))
37265				      (CDR L)))
37267		     (T(CONS(CAR L)(ELEVA C(CDR L)))))  )
37269	EXPR)
37271	
37273	
37275	(DEFPROP ELEVB
37277	   (LAMBDA(C L)
37279		(COND((NULL L)NIL)
37281		     ((AND(NULL(CDDAR L))(EQUAL(CADAR C)(CAAAR L)))
37283		      (SETQ SREL(NRCONJ(CADAR L)(CADR C)))
37285		      (CDR L))
37287		     (T(CONS(CAR L)(ELEVB C(CDR L)))))  )
37289	EXPR)
37291	
37293	
37295	(DEFPROP ELEVC
37297	   (LAMBDA(C L)
37299		(COND((NULL L)NIL)
37301		     ((AND(NULL(CDDAR L))(EQUAL(CAR C)(CAAR L)))
37303		      (SETQ SREL(NRCONJ(CADAR L)(CADR C)))
37305		      (SETQ SW T)
37307		      (CDR L))
37309		     (T(CONS(CAR L)(ELEVC C(CDR L)))))  )
37311	EXPR)
37313	
37315	
37317	(DEFPROP NRCONJ
37319	   (LAMBDA(R1 R2)
37321		(COND((NULL R2)R1)
37323		     ((MEMBER(CAR R2)R1)(NRCONJ R1(CDR R2)))
37325		     (T(CONS(CAR R2)(NRCONJ R1(CDR R2)))))  )
37327	EXPR)
37329	
37331	
37345	(DEFPROP WHILASSEM
37350	   (LAMBDA(BP IP CL CT )
37400	      (PROG(ALP ALS PA Y Z W R SASG SASGR TE ALF BET WFT ALFT RP)
37410	(PRINT @L37410)(PRINT BP)(PRINT IP)(PRINT CL)(PRINT CT)
37415	(PRINT @L37415)(PRINT(THV SASSERTLITS))(PRINT(THV ASSERTLITS))
37423		(SETQ WFT(THV FT))
37425	(PRINT @L37425)(PRINT CL)(PRINT WFT)
37427		(SETQ IP(REVERSE IP))
37431	WH2	(SETQ PA(CAR CL))
37432	(PRINT @L37432)(PRINT PA)(PRINT WFT)
37435		(SETQ Y(READLIST(APPEND(LIST @Y)(EXPLODE(THSETQ(THV YN)(ADD1(THV YN)))))))
37437		(SETQ Z(READLIST(APPEND(LIST @Z)(EXPLODE(THSETQ(THV ZN)(ADD1(THV ZN)))))))
37440		(COND((CDDR PA)(SETQ ALF(CAR PA))(SETQ BET(CADR PA)))
37443		     (T(SETQ ALF(CAAR PA))(SETQ BET(CADAR PA))))
37444		(SETQ ALFT(COND((CDDAR WFT)(CAAR WFT))(T(CAAAR WFT))))
37446		(SETQ BP(CONS(LIST @← Y ALFT)BP))
37447		(SETQ LIFOL(CONS(COND((THASVAL(THV NT))(SUBST Y ALFT(SUBST Z ALF(CAR LIFOL) )))
37448			(T(SUBST Y ALFT(SUBST Z BET(CAR LIFOL)))))  (CDR LIFOL)))
37449		(SETQ IP(APPEND IP(LIST(LIST @← Y Z))))
37452		(SETQ ALP(CONS(CONS ALF Y)ALP))
37455		(SETQ ALS(CONS(CONS BET Z)ALS))
37456	(PRINT @L37456)(PRINT PA)
37458		(COND((CDDR PA)(SETQ SASG(APPEND(LIST(LIST @← Z(CADDR PA)))
37461						     SASG))(GO WH4)))
37464		(SETQ R(CADR PA))
37467		(SETQ R(APPEND(LIST(CAR R))(COND((CDR R)(COND((CDDR R)(LIST @∧ (CADR R) @∧ (CADDR R)))
37470							     (T(LIST @∧ (CADR R)))))
37473						(T NIL))))
37475		(SETQ W(READLIST(APPEND(LIST @W)(EXPLODE(THV ZN)))))
37477		(SETQ RP R)
37478		(SETQ R(SUBST W BET R))
37479		(COND((EQUAL R RP)(SETQ R(SUBST W ALF R))))
37481		(SETQ SASGR(APPEND (LIST(LIST @IF R @THEN(LIST @← Z W)))SASGR))
37482	WH4	(SETQ CL(CDR CL))
37483		(SETQ WFT(CDR WFT))
37485		(COND(CL(GO WH2)))
38525	(PRINT @L38525)(PRINT ALP)(PRINT ALS)(PRINT SASG)(PRINT SASGR)
38530		(SETQ ALP(DEQ ALP))
38533		(SETQ ALS(DEQ ALS))
38550		(SETQ SASG(REVERSE(VSUB ALP SASG)))
38575		(SETQ SASGR(REVERSE(VSUB ALP SASGR)))
38600		(SETQ IP(VSUB ALS IP))
38625		(SETQ IP(VSUB ALP IP))
38650		(SETQ CT(VSUB ALP CT))
38700		(SETQ TE(SUBPLANL(APPEND(LIST(LIST @WHILE(CONS NEGSGN  CT)@DO(APPEND SASG IP SASGR)))(APPEND SASGR BP))(THV PLANL)))
38712	(PRINT TE)
38725		(RETURN TE) ))
38750	EXPR)
38752	
38754	
38756	(DEFPROP DEQ
38758	   (LAMBDA(SAL)
38760		(COND((NULL SAL)NIL)
38762		     (T(CONS(CAR SAL)(DEQ(DEQ1(CAR SAL)(CDR SAL)))))))
38764	EXPR)
38766	
38768	(DEFPROP DEQ1
38770	   (LAMBDA(A D)
38772		(COND((NULL D)NIL)
38774		     ((EQUAL(CAR A)(CAAR D))(DEQ1 A(CDR D)))
38776		     (T(CONS(CAR D)(DEQ1 A(CDR D))))))
38778	EXPR)
38780	
38796	
38808	(DEFPROP COMPCHANGES
38811	   (LAMBDA(IN1 IN2 ACL)
38814	      (PROG(CL1 L1 L2 UL UA A1 A2 LCL SREL SW CREL)
38815	(PRINT @L38815)(PRINT ACL)(PRINT IN1)(PRINT IN2)
38817	CO2	(SETQ L1(CAR IN1))   (SETQ L2(CAR IN2))
38820		(SETQ UL(ELASSOC L2 ACL))
38821		(SETQ LCL NIL) 
38822		(SETQ CREL(COND((EQ @R(CAR(REVERSE L1)))(REVERSE(CDR(REVERSE L1))))
38823			       (T L1)))
38824		(SETQ L1(CDR L1))   (SETQ L2(CDR L2))
38826		(COND((EQUAL L1 L2)(GO CO8)))
38829	CO4	(SETQ A1(CAR L1))  (SETQ A2(CAR L2))   (SETQ SW NIL)
38832		(SETQ UA(COND(UL(CAR UL))(T NIL)))
38834	(PRINT @L38834)(PRINT CL1)(PRINT LCL)(PRINT A1)(PRINT A2)(PRINT UA)
38835		(COND((EQUAL A1 A2)(GO CO6)))
38838		(COND((AND(NULL UA)(OR(NOT(EQUAL(SUBST @# A1 A2)A2))
38841				      (NOT(EQUAL(SUBST @# A2 A1)A1))))
38844		      (GO CO6)))
38847		(COND((AND UA(ATOM UA)(NOT(EQUAL(SUBST @# A1 A2)A2)))
38850		      (COND((AND(NOT(FINDC(LIST A1 A2 NIL)CL1))
38853			        (NOT(FINDC(LIST A1 A2 NIL)LCL)))
38856			    (SETQ LCL(CONS(LIST A1 A2 A2)LCL))
38859			    (GO CO6))
38862			   (T(GO CO6)))  ))
38865		(COND((AND UA(ATOM UA))(GO CO6)))
38868		(COND((AND(NOT(ATOM UA))(NOT(MEMBER(LIST A1 A2 UA)CL1))
38871			  (NOT(MEMBER(LIST A1 A2 UA)LCL)))
38874		      (SETQ CL1(DELL(LIST A1 A2 NIL)CL1))
38877		      (SETQ CL1(DELL(LIST(LIST A1 A2)NIL)CL1))
38880		      (SETQ LCL(DELL(LIST A1 A2 NIL)LCL))
38883		      (SETQ LCL(CONS(LIST A1 A2 UA)LCL))
38886		      (GO CO6)))
38889		(COND((AND(NULL UA)(OR(FINDC(LIST A1 A2 NIL)CL1)
38892				      (FINDC(LIST(LIST A1 A2)(LIST CREL))CL1)))
38895		      (GO CO6)))
38898		(COND((NULL UA)(SETQ SREL (LIST CREL)))
38901		     (T(GO CO6)))
38904		(SETQ CL1(ELEVA(LIST(LIST A1 A2)SREL)CL1))
38907		(COND(SW(GO CO6)))
38910		(SETQ LCL(ELEVA(LIST(LIST A1 A2)SREL)LCL))
38913		(COND(SW(GO CO6)))
38916		(SETQ CL1(ELEVB(LIST(LIST A1 A2)SREL)CL1))
38919		(SETQ LCL(ELEVB(LIST(LIST A1 A2)SREL)LCL))
38922		(SETQ CL1(ELEVC(LIST(LIST A1 A2)SREL)CL1))
38925		(SETQ LCL(ELEVC(LIST(LIST A1 A2)SREL)LCL))
38928		(COND(SW(SETQ LCL(CONS(LIST(LIST A1 A2)SREL)LCL))(GO CO6)))
38929		(SETQ LCL(CONS(LIST(LIST A1 A2)SREL)LCL))
38931	CO6	(SETQ L1(CDR L1))    (SETQ L2(CDR L2))
38934		(COND(UL(SETQ UL(CDR UL))))
38937		(COND(L1(GO CO4)))
38940		(SETQ CL1(APPEND LCL CL1))
38943	CO8	(SETQ IN1(CDR IN1))
38946		(SETQ IN2(CDR IN2))
38947		(COND(IN1(GO CO2)))
38948		(RETURN CL1)  ))
38949	EXPR)
38950	(DEFPROP REM#
39000	   (LAMBDA(A)
39050		(COND((ATOM A)A)
39100		     ((EQ @#(CAR A))(CADDR A))
39150		     (T(CONS(REM#(CAR A))(REM#(CDR A))))))
39200	EXPR)
39250	
39255	
39257	(DEFPROP AMBIG
39259	   (LAMBDA(CHL)
39261		(COND((NULL CHL)NIL)
39263		     ((AMBIG1(CAR CHL)(CDR CHL))T)
39265		     (T(AMBIG(CDR CHL))))  )
39267	EXPR)
39269	
39271	(DEFPROP AMBIG1
39273	   (LAMBDA(AC DC)
39275		(COND((NULL DC)NIL)
39277		     ((AMBIG2(AMBIG3 AC)(AMBIG3(CAR DC)))T)
39279		     (T(AMBIG1 AC(CDR DC))))  )
39281	EXPR)
39283	
39285	(DEFPROP AMBIG2
39287	   (LAMBDA(P1 P2)
39289		(OR(EQUAL(CAR P1)(CAR P2))  (EQUAL(CADR P1)(CADR P2))
39291		   (EQUAL(CAR P1)(CADR P2))(EQUAL(CADR P1)(CAR P2))    )  )
39293	EXPR)
39295	
39297	(DEFPROP AMBIG3
39299	   (LAMBDA(C)
39301		(COND((CDDR C)(LIST(CAR C)(CADR C)))
39302		     (T(CAR C)))  )
39303	EXPR)
39304	
39305	(DEFPROP REMBT
39306	   (LAMBDA(A)
39309	      (PROG NIL
39310		(GO RE1)
39312		(THDO(PRED1ARG P1A))
39315		(THDO(PRED2ARG P2A))
39318		(THDO(PRED3ARG P3A))
39321		(THDO(PRED4ARG P4A))
39324		(THDO(PRED5ARG P5A))
39327	RE1	(RETURN(REM# A))   ))
39330	EXPR)
39333	
39336	
39339	(DEFPROP PRED1ARG
39342	   (LAMBDA(X)
39345	      (THPROG(P)
39348		(THAMONG(THV P)X)
39351	A	(THFIND ALL
39354			(THEV(THDO
39357			   (THERASE((THV P)(THV Y1)))
39360			   (THASSERT((THV P)(THEV(CADDR(THV Y1)))))  ))
39363			(Y1)
39366			(THGOAL((THV P)(THNV Y1)))
39369			(EQ @#(CAR(THV Y1)))  )
39372		(THFINALIZE THTAG A)
39375		(THFAIL)   ))
39378	EXPR)
39381	
39384	
39387	(DEFPROP PRED2ARG
39390	   (LAMBDA(X)
39393	      (THPROG(P)
39396		(THAMONG(THV P)X)
39399	A	(THFIND ALL
39402			(THEV(THDO
39405			   (THERASE((THV P)(THV Y1)(THV Y2)))
39408			   (THASSERT((THV P)(THEV(CHECK#(THV Y1)))
39411					    (THEV(CHECK#(THV Y2))) ))  ))
39414			(Y1 Y2)
39417			(THGOAL((THV P)(THNV Y1)(THNV Y2)))
39420			(THOR(EQ @#(CAR(THV Y1)))(EQ @#(CAR(THV Y2)))) )
39423		(THFINALIZE THTAG A)
39426		(THFAIL)   ))
39429	EXPR)
39432	
39435	
39438	(DEFPROP PRED3ARG
39441	   (LAMBDA(X)
39444	      (THPROG(P)
39447		(THAMONG(THV P)X)
39450	A	(THFIND ALL
39453			(THEV(THDO
39456			   (THERASE((THV P)(THV Y1)(THV Y2)(THV Y3)))
39459			   (THASSERT((THV P)(THEV(CHECK#(THV Y1)))
39462					    (THEV(CHECK#(THV Y2)))
39463					    (THEV(CHECK#(THV Y3))) ))  ))
39465			(Y1 Y2 Y3)
39468			(THGOAL((THV P)(THNV Y1)(THNV Y2)(THNV Y3)))
39471			(THOR(EQ @#(CAR(THV Y1)))(EQ @#(CAR(THV Y2)))(EQ @#(CAR(THV Y3)))) )
39474		(THFINALIZE THTAG A)
39477		(THFAIL)   ))
39480	EXPR)
39483	
39486	
39489	(DEFPROP PRED4ARG
39492	   (LAMBDA(X)
39495	      (THPROG(P)
39498		(THAMONG(THV P)X)
39501	A	(THFIND ALL
39504			(THEV(THDO
39507			   (THERASE((THV P)(THV Y1)(THV Y2)(THV Y3)(THV Y4)))
39510			   (THASSERT((THV P)(THEV(CHECK#(THV Y1)))
39513					    (THEV(CHECK#(THV Y2)))
39516					    (THEV(CHECK#(THV Y3)))
39517					    (THEV(CHECK#(THV Y4))) ))  ))
39519			(Y1 Y2 Y3 Y4)
39522			(THGOAL((THV P)(THNV Y1)(THNV Y2)(THNV Y3)(THNV Y4)))
39525			(THOR(EQ @#(CAR(THV Y1)))(EQ @#(CAR(THV Y2)))(EQ @#(CAR(THV Y3)))(EQ @#(CAR(THV Y4)))) )
39528		(THFINALIZE THTAG A)
39531		(THFAIL)   ))
39534	EXPR)
39536	
39538	
39540	(DEFPROP PRED5ARG
39542	   (LAMBDA(X)
39544	      (THPROG(P)
39546		(THAMONG(THV P)X)
39548	A	(THFIND ALL
39550			(THEV(THDO
39552			   (THERASE((THV P)(THV Y1)(THV Y2)(THV Y3)(THV Y4)(THV Y5)))
39554			   (THASSERT((THV P)(THEV(CHECK#(THV Y1)))
39556					    (THEV(CHECK#(THV Y2)))
39558					    (THEV(CHECK#(THV Y3)))
39560					    (THEV(CHECK#(THV Y4)))
39561					    (THEV(CHECK#(THV Y5))) ))  ))
39562			(Y1 Y2 Y3 Y4 Y5)
39564			(THGOAL((THV P)(THNV Y1)(THNV Y2)(THNV Y3)(THNV Y4)(THNV Y5)))
39566			(THOR(EQ @#(CAR(THV Y1)))(EQ @#(CAR(THV Y2)))(EQ @#(CAR(THV Y3)))(EQ @#(CAR(THV Y4)))(EQ @#(CAR(THV Y5)))) )
39568		(THFINALIZE THTAG A)
39570		(THFAIL)   ))
39572	EXPR)
39574	
39576	
39578	
39590	(DEFPROP TRSUBSTP
39600	   (LAMBDA(PL ELT)
39650		NIL)
39700	EXPR)
39750	
39800	
39850	
39900	(DEFPROP TRSUBST
39950	   (LAMBDA(NE OE PL)
40000		(SUBST NE OE PL))
40050	EXPR)
40100	
40150	
40200	
40250	(DEFPROP SUBSTP
40300	   (LAMBDA(P V)
40350		(COND((EQUAL P V)T)
40400		     ((ATOM P)NIL)
40450		     (T(OR(SUBSTP(CAR P)V)(SUBSTP(CDR P)V)))))
40500	EXPR)
40550	
40600	
40650	
41050	
41100	(DEFPROP VSUB
41150	   (LAMBDA(RL PL)
41200	      (PROG(CRL SPL DONE CRL1)
41225		(COND((NULL PL)(RETURN NIL)))
41250		(SETQ CRL RL)
41300		(SETQ SPL PL)
41350	VS1	(COND(DONE(GO VS3)))
41400		(SETQ DONE T)
41450		(SETQ CRL(RECSUB1 CRL CRL))
41500		(GO VS1)
41550	VS3	(COND((NOT DONE)(RETURN SPL)))
41600		(SETQ CRL1 CRL)
41650		(SETQ DONE NIL)
41700	VS5	(COND((NULL CRL1)(GO VS3)))
41750		(COND((OR(SUBSTP SPL(CAAR CRL1))(TRSUBSTP SPL(CAAR CRL1)))(SETQ DONE T)))
41800		(SETQ SPL(TRSUBST(CDAR CRL1)(CAAR CRL1)SPL))
41850		(SETQ CRL1(CDR CRL1))
41900		(GO VS5)    ))
41950	EXPR)
42000	
42050	
42100	(DEFPROP RECSUB1
42150	   (LAMBDA(RL1 RL2)
42200		(COND((NULL RL1)RL2)
42250		     (T(RECSUB1(CDR RL1)(APPEND(RECSUB2(CAR RL1)RL2)RL2))))  )
42300	EXPR)
42350	
42400	
42450	(DEFPROP RECSUB2
42500	   (LAMBDA(RL11 RL22)
42550		(COND((NULL RL22)NIL)
42600		     ((AND(OR(SUBSTP(CAAR RL22)(CAR RL11))(TRSUBSTP(CAAR RL22)(CAR RL11)))(NOT(EQ(CDR RL11)(CDAR RL22))))
42650		      ((LAMBDA(S)(COND((MEMBER S RL2)(RECSUB2 RL11(CDR RL22)))
42700				      (T(APPEND(SETQ DONE NIL)(LIST S)
42750					       (RECSUB2 RL11(CDR RL22))))))
42800				 (TRSUBST(CDR RL11)(CAR RL11)(CAR RL22))))
42850		     (T(RECSUB2 RL11(CDR RL22))))  )
42900	EXPR)
42950	
43000	
43050	(OPS (TDNE 612000)(TTCALL 51000))
43100	(LAP TTYIN SUBR)
43150	(TTCALL 2 1)
43200	(CLEARM 0 1)
43250	(TDNE 1 '(C 777777 0 777760))
43300	(POPJ P 0)
43350	(CLEARM 0 1)
43400	(POPJ P 0)
43450	NIL
43500	
43550	
43600	(DEFPROP CJOINCOND
43650	   (LAMBDA NIL
43700	      (PROG(PD LDB LA)
43750	JO3	(SETQ LDB(CADAR(THV PROCDATA)))
43800		(SETQ LA(CADDAR(THV PROCDATA)))
43850		(COND((EQUAL(LENGTH LDB)(LENGTH(THV DBLITS)))(PRINT @YES)(GO JO6)))
43900		(SETQ LDB(REVERSE(INCRELIT LDB(REVERSE(THV DBLITS)))))
43950		(SETQ LA(REVERSE(INCRELIT LA(REVERSE(THV ASSERTLITS)))))
44000		(SETQ LDB(DBREF LDB LA))
44050		(SETQ JOINCOND(CONS(LIST(CAAR(THV PROCDATA))LDB)JOINCOND))
44100	JO6	(THSETQ(THV PROCDATA)(CDR(THV PROCDATA))T T)
44150		(COND((THV PROCDATA)(GO JO3)))
44200		(RETURN T)   ))
44250	EXPR)
44300	
44350	
44400	(DEFPROP INCRELIT
44450	   (LAMBDA(L B)
44500		(COND((NULL L)B)
44550		     (T(INCRELIT(CDR L)(CDR B))))  )
44600	EXPR)
44610	
44612	
44614	(DEFPROP STORPLIB
44616	   (LAMBDA NIL
44618	     (PROG(PRO)
44619		(COND((NULL COMPI)(ED T)))
44620		(OUTC @PLIB NIL)
44624		(SETQ PRO(LIST @DEFPROP PL
44626		   (APPEND(LIST @THCONSE)
44628			  (LIST GVARL)
44630			  (LIST(CAR TAS))
44632			  (IAS(APPEND TYP STA))
44634			  (LIST(LIST @THSET @(CAR(THV ANS))(LIST @APPEND @(EVAL(CAR(THV ANS)))
44636					(LIST @REVERSE(LIST @INSTPROG(LIST @QUOTE PANS)(LIST  @QUOTE GVARL) )))))
44638			  (OAS TAS))
44640		   @THEOREM))
44642		(SPRINT PRO 2 1)
44644		(PRINT(LIST @THASSERT PL))
44646		(OUTC NIL NIL)   ))
44648	EXPR)
44650	
44652	
44654	(DEFPROP IAS
44656	   (LAMBDA(IA)
44658		(COND((NULL IA)NIL)
44660		     (T(CONS(LIST @THGOAL(CAR IA)@(THTBF THTRUE))(IAS(CDR IA)))))  )
44668	EXPR)
44670	
44672	
44674	(DEFPROP INSTPROG
44676	   (LAMBDA(PA VARL)
44678		(COND((NULL VARL)PA)
44680		     (T(INSTPROG(SUBST(EVAL(LIST @THV(CAR VARL)))(LIST @THV(CAR VARL))PA)(CDR VARL))))  )
44682	EXPR)
44684	
44686	
44688	
44690	(DEFPROP OAS
44692	   (LAMBDA(TAS)
44694		(COND((NULL TAS)NIL)
44696		     (T(CONS(LIST @THASSERT(CAR TAS))(OAS(CDR TAS)))))  )
44700	EXPR)
44702	
44704	
44750	(DEFPROP GENERALIZE
44800	   (LAMBDA NIL 
44850	      (PROG (TAS TDB CL VN VA PANS TYP STA TEM TEM1 GPAR GVARL)
44900		(PRINT @IS_THIS_PLAN_USEFUL_ENOUGH_TO_BE_GENERALIZED?*)
44950		(COND((READ)(SETQ GSWI GANS))
45000		     (T(GO GE9)))
45050		(PRINT @DO_YOU_WANT_TO_SEE_THE_GENERALIZED_VERSION?*)
45100		(COND((READ)(SETQ GGEN T))(T(SETQ GGEN NIL)))
45150		(SETQ TDB(DBREF(THV DBLITS)(APPEND(THV WASSERTLITS)(THV ASSERTLITS))))
45200		(SETQ TAS(REVERSE(NETASSERT(THV ASSERTLITS))))
45250		(SETQ TEM(APPEND TDB TAS))
45300	GE4	(SETQ CL(APPEND(CONSTL(CDAR TEM))CL))
45350		(SETQ TEM(CDR TEM))
45400		(COND(TEM(GO GE4)))
45410		(SETQ GENAL(REVERSE(CDR(REVERSE(CDR (CAR TAS))))))
45419	(PRINT @L45419)(PRINT GOL)(PRINT TDB)(PRINT TAS)	(SETQ GPAR @ALL)
45420		(PRINT @IS_THIS_A_PROCEDURE_WITHOUT_SIDE_EFFECTS?*)
45421		(COND((READ)(SETQ GPAR (CDR(REVERSE(CDR(REVERSE GOL)))))))
45422		(COND((NOT(EQ GPAR @ALL))(SETQ CL GPAR)(SETQ TDB(ELIMLOCALPAR TDB))(SETQ TAS(ELIMLOCALPAR TAS))))
45450		(SETQ GCON(REVERSE CL))
45460	(PRINT @L45460)(PRINT GANS)(PRINT TDB)(PRINT TAS)
45500		(SETQ PANS GANS)
45550		(SETQ VN 0)   (SETQ IGTDB TDB)  (SETQ IGTAS TAS)
45600		(SETQ GTDB TDB)(SETQ GTAS TAS)(SETQ GVL NIL)(SETQ GTYP NIL)(SETQ GSTA NIL)
45650	GE5	(SETQ VA(LIST @THV(READLIST(APPEND @(V)(EXPLODE(SETQ VN(ADD1 VN)))))))
45700		(SETQ TDB(SUBST VA(CAR CL)TDB))
45750		(SETQ TAS(SUBST VA(CAR CL)TAS))
45800		(SETQ PANS(SUBST VA(CAR CL)PANS))
45850		(SETQ VA(CADR VA))
45860		(SETQ GVARL(CONS VA GVARL))
45900		(SETQ GVL(CONS VA GVL))
45950		(SETQ GTDB(SUBST VA(CAR CL)GTDB))
46000		(SETQ GTAS(SUBST VA(CAR CL)GTAS))
46050		(SETQ GSWI(SUBST VA(CAR CL)GSWI))
46100		(SETQ CL(CDR CL))
46150		(COND(CL(GO GE5)))
46160		(SETQ GENAL(COND((ATOM GTAS)NIL)(T(REVERSE(CDR(REVERSE(CDAR GTAS)))))))
46200		(SETQ TEM TDB) (SETQ TEM1 GTDB)
46250	GE6	(COND((EQ @R(CAR(REVERSE(CAR TEM))))(SETQ STA(CONS(CAR TEM)STA)))
46300		     (T(SETQ TYP(CONS(CAR TEM)TYP))))
46350		(COND((EQ @R(CAR(LAST(CAR TEM1))))(SETQ GSTA(CONS(CAR TEM1)GSTA)))
46400		     (T(SETQ GTYP(CONS(CAR TEM1)GTYP))))
46450		(SETQ TEM(CDR TEM))
46500		(SETQ TEM1(CDR TEM1))
46550		(COND(TEM(GO GE6)))
46600		(SETQ TAS(REVERSE TAS))
46650		(SETQ GTAS(REVERSE GTAS))
46660	(PRINT @L46660)(PRINT TAS)(PRINT TYP)(PRINT STA)
46700		(STORPLIB)
46750	GE9	(SETQ READY(CONS(CONS(LIST PL GOL ST)(LIST GANS))READY))  ))
46800	EXPR)
46850	
46852	
46854	(DEFPROP ELIMLOCALPAR
46856	   (LAMBDA(TL)
46858		(COND((NULL TL)NIL)
46860		     ((HASGLOB(CDAR TL))(CONS(CAR TL)(ELIMLOCALPAR(CDR TL))))
46862		     (T(ELIMLOCALPAR(CDR TL))))   )
46864	EXPR)
46866	
46868	
46870	
46872	(DEFPROP HASGLOB
46874	   (LAMBDA(LI)
46876		(COND((OR(NULL LI)(EQ(CAR LI)@R))T)
46878		     ((AND(NOT(ATOM(CAR LI)))(NOT(NUMBERP(CAAR LI))))(AND(HASGLOB(CAR LI))(HASGLOB(CDR LI))))
46880		     ((NOT(MEMBER(CAR LI)CL))NIL)
46882		     (T(HASGLOB(CDR LI))))  )
46884	EXPR)
46886	
46888	
46900	
46950	(DEFPROP DBREF
47000	   (LAMBDA(DB AS)
47050	      (PROG(TD1 TD2)
47100		(SETQ TD1(CARDBLIT DB))
47150		(SETQ TD1(NONREDUN(REVERSE TD1)))
47200	DB2	(COND((NOT(ELASSOC(CAR TD1)AS))
47250		      (SETQ TD2(CONS(CAR TD1)TD2))))
47300		(SETQ TD1(CDR TD1))
47350		(COND(TD1(GO DB2)))
47400		(RETURN TD2)   ))
47450	EXPR)
47500	
47502	
47504	
47506	
47508	(DEFPROP ELASSOC
47510	   (LAMBDA(L AL)
47512		(COND((NULL AL)NIL)
47514		     ((EQUAL L(CAAR AL))(CADAR AL))
47516		     (T(ELASSOC L(CDR AL))))  )
47518	EXPR)
47520	
47522	
47524	
47550	
47600	(DEFPROP NETASSERT
47650	   (LAMBDA(TA1)
47700		(COND((NULL TA1)NIL)
47750		     ((THVAL @(THGOAL(THEV(CAAR TA1))(THTBF FILTERAX))THALIST)
47800		      (CONS(CAAR TA1)(NETASSERT(CDR TA1))))
47850		     (T(NETASSERT(CDR TA1))))    )
47900	EXPR)
47950	
48000	
48050	
48100	(DEFPROP CONSTL
48150	   (LAMBDA(TX)
48200		(COND((NULL TX)NIL)
48250		     ((EQ @R(CAR TX))NIL)
48300		     ((MEMBER(CAR TX)CL)(CONSTL(CDR TX)))
48350		     ((NOT(ATOM(CAR TX)))(APPEND(CONSTL(CDAR TX))(CONSTL(CDR TX))))
48400		     (T(CONS(CAR TX)(CONSTL(CDR TX))))))
48450	EXPR)
48500	
48550	
48600	
48650	(DEFPROP CARDBLIT
48700	   (LAMBDA(DBL)
48750		(COND((NULL DBL)NIL)
48800		     (T(APPEND(CARDBLIT1(CAR DBL))(CARDBLIT(CDR DBL))))))
48850	EXPR)
48900	
48950	
49000	(DEFPROP CARDBLIT1
49050	   (LAMBDA(TDBL)
49100		(COND((NULL TDBL)NIL)
49150		     ((ATOM(CAR TDBL))(CARDBLIT1(CDR TDBL)))
49200		     (T(CONS(CAADAR TDBL)(CARDBLIT1(CDR TDBL))))))
49250	EXPR)
49300	
49350	
49400	(DEFPROP NONREDUN
49450	   (LAMBDA(DBL)
49500	      (PROG(NRL PDBL)
49550		(SETQ PDBL DBL)
49600	NO2	(COND((NOT(MEMBER(CAR PDBL)NRL))
49650		      (SETQ NRL(CONS(CAR PDBL)NRL))))
49700		(SETQ PDBL(CDR PDBL))
49750		(COND(PDBL(GO NO2)))
49800		(RETURN(REVERSE NRL))   ))
49850	EXPR)
49900	
49950	
50000	
50050	(DEFPROP OUTANS
50100	   (LAMBDA NIL
50150	      (PROG(GTYP1 GTYP1 GTAS1 IGTYP IGSTA IGTDB1 COMLST CLST)
50200		(TERPRI)
50250		(PRINT @THE_GOAL_)(PRINC (REVERSE(CDR(REVERSE GOL))))(PRINC @_IS_ATTAINABLE_BY_THE_FOLLOWING_PROGRAM:)
50300		(TERPRI)(TERPRI)
50340	(COND((ATOM PL)(PRINT PL))(T(PRINT(CAR PL))))
50350	(PRINC(REVERSE(CDR(REVERSE(CDR GOL)))))
50400		(COND((NULL GSWI)(GO OU41)))
50450		(SETQ IGTDB1 IGTDB)
50500	OU1	(COND((EQ @R(CAR(LAST(CAR IGTDB1))))(SETQ IGSTA(CONS(CAR IGTDB1)IGSTA)))
50550		     (T(SETQ IGTYP(CONS(CAR IGTDB1)IGTYP))))
50600		(SETQ IGTDB1(CDR IGTDB1))
50650		(COND(IGTDB1(GO OU1)))
50700		(TERPRI)
50750	OU12	(PRINC(CAAR IGTYP))  (PRINC(CDAR IGTYP))  (PRINC @;)
50800		(SETQ IGTYP(CDR IGTYP))
50850		(COND(IGTYP(GO OU12)))
50900		(PRINT @COMMENT)(PRINT @INPUT_CONDITIONS:)(TERPRI)
50950		(OUTCONDI IGSTA)
51000		(PRINT @OUTPUT_CONDITIONS:)(TERPRI)
51050		(OUTCONDI IGTAS)
51100		(PRINC @;)
51104	OU41	(COND((THV ASSL)(PRINT @COMMENT)
51107	              (PRINT @THIS_PROGRAM_RELIES_ON_THE_FOLLOWING_ASSUPTIONS:)(PRINT(THV ASSL))(PRINC @;)))
51110	    	(COND((THV COMMENTLIST)(PRINT @COMMENT))
51112	             (T(GO OU02)))
51113		(SETQ CLST(THV COMMENTLIST))
51115	OU4	(COND((NULL CLST)(PRINC @;)(GO OU02)))
51116		(TERPRI)
51120		(SETQ COMLST(CAR CLST))
51125		(THSETQ CLST(CDR CLST)T T)
51130	OU5	(COND((NULL COMLST)(GO OU4)))
51135		(PRINC(CAR COMLST))(PRINC @" ")
51140		(SETQ COMLST(CDR COMLST))
51145		(GO OU5)
51150	OU02	(SETQ INDENT NIL)
51200	   	(TSLPLAN GANS)
51250		(COND(STAT(TERPRI)
51300	                  (PRINT THME)(PRINC @__RULES_ENTERED)(PRINT THMS)(PRINC @__RULES_SUCCESSFUL)))
51400		(TERPRI)
51450		(COND((OR(NULL GSWI)(NULL GGEN))(RETURN T)))
51500		(SETQ GTYP1 GTYP) (SETQ GSTA1 GSTA) (SETQ GTAS1 GTAS)
51550		(PRINT @THIS_PLAN_HAS_ALSO_BEEN_GENERALIZED_AND_RESIDES_IN_THE)
51600		(PRINT @LIBRARY_IN_THE_FORM:)
51650		(TERPRI)
51690	(COND((ATOM PL)(PRINT PL))(T(PRINT(CAR PL))))
51700	(PRINC GENAL)
51725	(TERPRI)
51750	OU3	(PRINC(CAAR GTYP1))(PRINC(CDAR GTYP1))
51800		(PRINC @;) 
51850		(SETQ GTYP1(CDR GTYP1))
51900		(COND(GTYP1(GO OU3)))
51950		(PRINT @COMMENT)
52000		(PRINT @INPUT_CONDITIONS:)(TERPRI)
52050		(OUTCONDI GSTA1)
52100		(PRINT @OUTPUT_CONDITIONS:)(TERPRI)
52150		(OUTCONDI GTAS1)
52200		(PRINC @;)
52250	   	(TSLPLAN GSWI) (TERPRI)  ))
52300	EXPR)
52350	
52400	
52450	
52500	(DEFPROP OUTCONDI
52550	   (LAMBDA(CC)
52600	      (PROG(LCC)
52625		(COND((NULL CC)(PRINC @NONE)(RETURN T)))
52650		(SETQ LCC CC)
52700	OU00	(PRINC(CAAR LCC))
52750		(COND((EQ @R(CAR(LAST(CAR LCC))))
52800		      (PRINC(REVERSE(CDR(REVERSE(CDAR LCC))))))
52850		     (T(PRINC(CDAR LCC))))
52900		(SETQ LCC(CDR LCC))
52950		(COND(LCC(PRINC @∧)(GO OU00)))
53000		(RETURN T)  ))
53050	EXPR)
53100	
53150	
53200	
53250	
53300	
53350	(DEFPROP PROCJOIN
53400	   (LAMBDA NIL
53450	      (PROG(JC)
53500		(COND((NOT(SETQ JC(FINDCOND JOINCOND)))(RETURN T)))
53550		(SETQ SSW T)
53600		(SETQ JCFC(TESTJOIN JC))
53650		(SETQ SSW NIL)
53700		(COND((NULL JCFC)(RETURN T)))
53750		(RETURN NIL)  ))
53800	EXPR)
53850	
53900	
53950	(DEFPROP FINDCOND
54000	   (LAMBDA(JOC)
54050		(COND((NULL JOC)NIL)
54100		     ((MEMBER PL(CAAR JOC))(CADAR JOC))
54150		     (T(FINDCOND(CDR JOC)))))
54200	EXPR)
54250	
54300	(DEFPROP TESTJOIN
54350	   (LAMBDA(JC)
54400		(COND((NULL JC)NIL)
54450		     ((THVAL @(THGOAL(THEV(CAR JC)))THALIST)
54500		      (TESTJOIN(CDR JC)))
54550		     (T(CAR JC)))   )
54600	EXPR)
54650	
54655	(DEFPROP STEPREF
54658	   (LAMBDA(OPN ARGL GL)
54661	      (PROG(ST)
54662		(COND((AND(THV WF)(THASVAL(THV FT)))(RETURN T)))
54664	        (SETQ ST(READLIST(APPEND @(S T A T)(EXPLODE(SETQ SN(ADD1 SN))))))
54667	        (SAVESTATE ST)
54670	        (SETQ LIFOL(CONS(LIST(CONS OPN ARGL)GL ST)LIFOL))
54673	        (THSETQ(THV ASSL)(CONS OPN(THV ASSL)))
54676	        (RETURN T)  ))
54679	EXPR)
54682	
54685	(DEFPROP POPN
54688	   (LAMBDA NIL
54692	      (PROG(N)
54694	        (SETQ N(LENGTH(THV ASSL)))
54697	PO2     (COND((ZEROP N)(RETURN T)))
54700	        (SETQ N(SUB1 N))
54703	        (SETQ LIFOL(CDR LIFOL))
54706	        (GO PO2)   ))
54709	EXPR)
54712	
54715	
54750	(DEFPROP SUBGOAL
54800	   (LAMBDA (L)
54850	      (PROG(JCFC PL GOL ST PREDLIST LGANS LCT INDENT STAT THME THMS GANS RES FILENAME COMPI GENAL LIBFIT
54900	            PVARLIST GSWI GTDB GTAS GVL GCON GSTA GTYP GGEN IGTDB IGTAS FUNDEFLIST P1A P2A P3A P4A P5A)
54950		(CSYM NF00)
55000	SU0	(COND((EQ T(CAR L))(GO SU40)))
55050		(COND((AND(NOT(NULL L))(NOT(EQ @DSK:(CAR L))))(SETQ FILENAME(CAR L))(GO SU10)))
55100		(COND((NULL COMPI)(DSKIN COMPR)(ED T)(SETQ COMPI T)))
55150		(COMP L)
55200	SU10	(EVAL(LIST @DSKIN FILENAME))
55250		(COND((AND(NOT(NULL L))(NOT(EQ @DSK:(CAR L))))(RESTOREPROP)(REMPROP @RESTOREPROP @EXPR)))
55300		(OUTC(OUTPUT DSK: INIT)T)
55350		(THDUMP)
55400		(OUTC NIL)
55410		(OUTC(OUTPUT PLIB DSK: PLIB)NIL)
55420		(OUTC NIL NIL)
55450		(SETQ ST @INIT)
55500	SU12	(PRINT @SUBMIT_GOAL*)
55550		(SETQ GOL(READ))
55560		(SETQ LIBFIT NIL)
55600		(SETQ PL(READLIST(APPEND @(P R O C)(EXPLODE(SETQ PN(ADD1 PN))))))
55610		(PRINT @DO_YOU_WANT_TO_TRY_USING_THE_PROGRAM_LIBRARY?)
55630		(COND((READ)(SETQ LIBFIT T)(DSKIN PLIB)))
55650	SU13	(PRINT @DO_YOU_HAVE_ANY_ADVICE?*)
55700		(COND((READ)(ADVICESYS)))
55750	SU15	(SETQ THME 0)(SETQ THMS 0)
55760		(THVSETQ(THV COMMENTLIST)NIL)
55800	  	(SETQ THSTEPT @(STEPT))
55850		(COND((AND(GET(CAR GOL)@FLUENT)(NOT(EQ @R(CAR(LAST GOL)))))(SETQ GOL(APPEND GOL(LIST @R)))))
55900		(SETQ RES(THVAL(LIST @THGOAL GOL(LIST @THTBF @THTRUE))THALIST))
55950		(SETQ THSTEPT NIL)
56000		(COND((NULL RES)(GO SU17)))
56050		(COND((PROCJOIN)(GO SU16)))
56100		(PRINT @THE_JOIN_CONDITION_)(PRINC JCFC)(PRINC @_FAILED!)
56150		(PRINT @HENCE_THE_PROCEDURE_IN_ITS_PRESENT_FORM_CANNOT_BE_USED)
56200		(PRINT @DO_YOU_WANT_TO_EXTEND_THE_PROCEDURE_)(PRINC PL)(PRINC @_TO_SATISFY_)(PRINC JCFC)(PRINC @*)
56250		(COND((READ)(SETQ GOL JCFC)(SETQ JCFC NIL)(GO SU13)))
56300		(GO SU20)
56350	SU16	(COND((THV PROCDATA)(CJOINCOND)))
56450		(COND((NULL GANS)(PRINT @GOAL_TRUE_IN_PRESENT_WORLD!)(TERPRI)(GO SU20)))
56500		(PRINT @DO_YOU_WANT_TO_OPTIMIZE_THE_PROGRAM?*)
56510		(COND((READ)(SETQ GANS(OPTIM GANS))))
56520		(GENERALIZE)
56530		(GO SU18)
56550	SU17	(PRINT @THE_GOAL_FAILED!__DO_YOU_WANT_TO_TRY_AGAIN_WITH_MORE_ADVICE?*)
56600		(COND((READ)(ADVICESYS)(GO SU15)))
56658		(GO SU20)
56700	SU18	(OUTANS)
56725	(PRINT PL)
56750		(EVAL(LIST @OUTC(LIST @OUTPUT @DSK: (COND((ATOM PL)PL)(T(CAR PL))))T))
56800		(OUTANS)
56850		(OUTC NIL)
56852	        (COND((NULL(THV ASSL))(GO SU20)))
56855	        (PRINT @DO_YOU_WANT_TO_DO_STEPWISE_REFINEMENT:)
56858	        (COND((NULL(READ))(POPN)(GO SU20)))
56861	SU19    (SETQ PL(CAR LIFOL))
56864	        (SETQ LIFOL(CDR LIFOL))
56867	        (GO SU25)
56900	SU20	(COND((NULL FIFOL)(GO SU28)))
56950		(PRINT @DO_YOU_WANT_TO_DO_CONTINGENCY_PLANNING?*)
57000		(COND((NULL(READ))(GO SU30)))
57050		(THSETQ(THV DBLITS)NIL T T)
57100		(THSETQ(THV ASSERTLITS)NIL T T)
57150		(PRINT @WHAT_IS_YOUR_PREFERENCE?__IF_NONE_TYPE_NIL*)
57200	SU22	(SETQ PL(READ))
57225	(PRINT @L57225)(PRINT PL)
57250		(COND((NULL PL)(SETQ PL(CAR FIFOL))(PRINT NIL)(PRINT PL)(SETQ FIFOL(CDR FIFOL)))
57300		     ((SETQ PL(ASSOC PL FIFOL))(PRINT T)(PRINT PL)(SETQ FIFOL(DELAD1(CAR PL)FIFOL)))
57350		     (T(PRINT @NO_SUCH_PROC___TRY_AGAIN*)(GO SU22)))
57400	SU25	(SETQ GOL(CADR PL))
57450		(COND((EQUAL(LAST GOL)@(R))(SETQ GOL(REVERSE(CDR(REVERSE GOL))))))
57500		(THFLUSH THASSERTION THERASING THCONSE)
57525	(PRINT @L57525)(PRINT PL)
57550		(SETQ ST(CADDR PL))
57575	(PRINT @L57575)(PRINT ST)
57600		(PRINT @TRYING___)(PRINC PL)
57650		(EVAL(LIST @DSKIN ST))
57700		(SETQ PL(CAR PL))
57750		(SETQ GANS NIL)
57800		(THVSETQ(THV PROCDATA)NIL)
57825		(THVSETQ(THV PASSUM)NIL)
57828	        (THVSETQ(THV ASSL)NIL)
57850		(THVSET(CAR(THV ANS))NIL)
57900	(THSETQ(THV O1)@THUNASSIGNED)
57950		(SETQ LCT NIL)(SETQ LGANS NIL)
58000		(GO SU13)
58010	SU28    (COND((NULL(THV ASSL))(GO SU30)))
58013	        (PRINT @DO_YOU_WANT_TO_DO_STEPWISE_REFINEMENT:)
58016	        (COND((NULL(READ))(GO SU30)))
58019	        (GO SU19)
58050	SU30	(COND(JCFC(PRINT @INITIAL_STATE_REENTERED)(GO SU40)))
58100		(SETQ GANS NIL)
58150		(SETQ LCT NIL)(SETQ LGANS NIL)
58200		(PRINT @DO_YOU_WANT_TO_CONTINUE_FROM_THE_PRESENT_STATE_OF_THE_WORLD?)
58250		(COND((READ)(GO SU12)))
58300	SU40	(THFLUSH THASSERTION THERASING THCONSE)
58350		(THSETQ(THV DBLITS)NIL T T)
58400		(THSETQ(THV ASSERTLITS)NIL T T)
58450		(DSKIN INIT)
58500		(SETQ ST @INIT)
58550		(THVSETQ(THV PROCDATA)NIL)
58600		(THVSET(CAR(THV ANS))NIL)
58625		(THVSETQ(THV PASSUM)NIL)
58628	        (THVSETQ(THV ASSL)NIL)
58650		(GO SU12)
58700	))
58750	FEXPR)